$\forall$${\it es}$:ES, $A$, $B$:Type, ${\it Ia}$:AbsInterface($A$), ${\it Ib}$:AbsInterface($B$), $f$:(E(${\it Ia}$)$\rightarrow$$B$), $g$:(E(${\it Ib}$)$\rightarrow$E).
\\[0ex]glues(${\it es}$; $B$; $g$; $f$; ${\it Ia}$; ${\it Ib}$) $\Rightarrow$ ($g$ $\in$ E(${\it Ib}$)$\rightarrow$E(${\it Ia}$))